basic
Trans(T;x,y.E(x;y)) == a, b, c:T. E(a;b)  E(b;c)  E(a;c) 

latex

---

clarification:

basic
Trans(T;x,y.E(x;y)) == a:T. b:T, c:T. E(a;b)  E(b;c)  E(a;c) 

latex

Up	rel 1, rel 1
Wellformedness Lemmas	trans wf, trans wf
Definitions	x:A. B(x), P  Q
FDL editor aliases	trans